module Data.Transform.CheckRules where

import HUnit
import Data.Transform.Type
import Data.Transform.TwoLevel
import Data.Transform.RulesPF (simplifyPF)

checkRuleWithValues ::(Eq a,Show a) =>  Rule -> (Type a) -> [a] -> Assertion
checkRuleWithValues r tp v = do
                                let (Just view) = r tp 
                                let bs = forths view v
                                let as = backs view bs
                                assertEqual "Values should be the same" as v

backs ::  View (Type a) -> [Dynamic] -> [a]
backs view bs = unMaybes(map (backDyn view) bs)

forths :: View (Type a) ->  [a] -> [Dynamic]
forths view as = unMaybes(map (forthDyn view) as)


unMaybes::[Maybe a] -> [a]
unMaybes ((Just a):t) = a:(unMaybes t)
unMaybes (Nothing:t) = unMaybes t
unMaybes [] =[]





checkRuleWithProof::(Eq a,Show a)=> Rule -> (Type a) -> Assertion
checkRuleWithProof r ta =do (View rep tb) <- (\(Just x) -> return x) (r ta)
                            let (Rep f t) = rep
                            let ft = FUN "" (f . t)    
                            let (Just sft) = simplifyPF (Func tb tb) ft
                            assertBool "from.to != id"  (geq (PF (Func tb tb)) ID sft)

